/******************************************************************************

    Copyright (C) 2006 Alessio Stalla (alessiostalla@gmail.com)

    This file is part of PrettyProlog.

    PrettyProlog is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    PrettyProlog is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with PrettyProlog; if not, write to the Free Software
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA

    See the file COPYING for further details.

 *****************************************************************************/

package prettyprolog.engine.syspreds;

import java.util.Iterator;
import java.util.List;

import prettyprolog.datatypes.Callable;
import prettyprolog.datatypes.Substitution;
import prettyprolog.datatypes.Term;
import prettyprolog.engine.Clause;
import prettyprolog.engine.Engine;
import prettyprolog.engine.NotAClauseException;
import prettyprolog.engine.Theory;
import prettyprolog.engine.UnificationAlgorithm;

/**
 * Implements the retract/1 system predicate. It eliminates from the Theory the
 * first clause which unifies with its argument. A clause can be specified
 * either in prefix form (<code>:-(Head, Body)</code>) or infix form (
 * <code>Head :- Body</code>). Note that <code>a.</code> and
 * <code>a :- true.</code> are different clauses and don't unify.
 */
public class Retract extends SystemPredicate {

	private static final Retract inst = new Retract();

	private Retract() {
		super(1);
	}

	/** Returns the only instance of this system predicate. */
	public static Retract getInstance() {
		return inst;
	}

	/**
	 * @throws SyspredException
	 *             if the argument is not a clause.
	 */
	public SyspredEffect doCall(Engine en, Substitution subst, List<Term> args)
			throws SyspredException {
		SyspredEffect effct = new SyspredEffect(true, subst);
		Theory th = en.getTheory();
		UnificationAlgorithm unif = en.getUnificationAlgorithm();
		Term t = args.get(0);
		if (t instanceof Callable) {
			Clause c;
			try {
				c = new Clause((Callable) t, en.getClauseSymbol());
			} catch (NotAClauseException _e) {
				throw new SyspredException(t + " is not a clause.");
			}
			Iterator<Clause> th_it = th.iterator();
			while (th_it.hasNext()) {
				Clause cl = th_it.next();
				Substitution subst_tmp = unif.unify(c.getHead(), cl.getHead());
				// if the heads unify...
				if (subst_tmp != null) {
					Substitution subst_new = subst.compose(subst_tmp);
					subst_tmp = unif.unify(c.getBody(), cl.getBody());
					// if the bodies unify &
					// the new subst doesn't contradict the old one...
					if (subst_tmp != null && subst_new != null) {
						subst_new = subst_new.compose(subst_tmp);
						// if the new subst doesn't contradict the old one
						// we're done
						if (subst_new != null) {
							effct.setFailFlag(false);
							effct.setSubstitution(subst_new);
							th.retract(cl);
							return effct;
						}
					}
				}
			}
		}
		return effct;
	}

	public boolean isBacktrackable() {
		return true;
	}

	public String toString() {
		return super.toString() + " retract";
	}
}